Problem:
 g(f(x,y),z) -> f(x,g(y,z))
 g(h(x,y),z) -> g(x,f(y,z))
 g(x,h(y,z)) -> h(g(x,y),z)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    h1(5,1) -> 5,3
    h1(6,2) -> 5,3
    h1(5,2) -> 5,3
    h1(6,1) -> 5,3
    g1(1,2) -> 5*
    g1(1,10) -> 5,3
    g1(2,1) -> 5*
    g1(2,9) -> 5,3
    g1(1,1) -> 6*
    g1(1,9) -> 5,3
    g1(2,2) -> 5*
    g1(2,10) -> 5,3
    f1(1,2) -> 10*
    f1(1,6) -> 6,3
    f1(1,10) -> 9*
    f1(2,1) -> 9*
    f1(2,3) -> 3*
    f1(2,5) -> 5,6,3
    f1(2,9) -> 9*
    f1(1,1) -> 9*
    f1(1,3) -> 3*
    f1(1,5) -> 5,6,3
    f1(1,9) -> 9*
    f1(2,2) -> 9*
    f1(2,6) -> 6,3
    f1(2,10) -> 9*
    g0(1,2) -> 3*
    g0(2,1) -> 3*
    g0(1,1) -> 3*
    g0(2,2) -> 3*
    f0(1,2) -> 1*
    f0(2,1) -> 1*
    f0(1,1) -> 1*
    f0(2,2) -> 1*
    h0(1,2) -> 2*
    h0(2,1) -> 2*
    h0(1,1) -> 2*
    h0(2,2) -> 2*
  problem:
   
  Qed